T:Type, L, L1, L2:T List. interleaving(T;L1;L2;L)  ||L|| = ||L1||+||L2||   

latex

Definitions	t  T, x:A. B(x), ||as||, ij, P  Q, False, A, AB, , disjoint_sublists(T;L1;L2;L), Prop, P & Q, interleaving(T;L1;L2;L)
Lemmas	nat wf, disjoint sublists wf, non neg length, length wf1